0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 84 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 23 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 MRRProof (⇔, 84 ms)
↳22 QDP
↳23 DependencyGraphProof (⇔, 2 ms)
↳24 QDP
↳25 UsableRulesProof (⇔, 0 ms)
↳26 QDP
↳27 QReductionProof (⇔, 0 ms)
↳28 QDP
↳29 QDPSizeChangeProof (⇔, 0 ms)
↳30 YES
samefringeC_in_gg(nil, nil) → samefringeC_out_gg(nil, nil)
samefringeC_in_gg(cons(T7, T8), cons(T9, T10)) → U6_gg(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17) → U2_ggaaggaa(T15, T9, T10, X16, X17, gopherA_in_ggaa(T9, T10, X16, X17))
gopherA_in_ggaa(nil, T22, nil, T22) → gopherA_out_ggaa(nil, T22, nil, T22)
gopherA_in_ggaa(cons(T29, T30), T31, X44, X45) → U1_ggaa(T29, T30, T31, X44, X45, gopherA_in_ggaa(T29, cons(T30, T31), X44, X45))
U1_ggaa(T29, T30, T31, X44, X45, gopherA_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherA_out_ggaa(cons(T29, T30), T31, X44, X45)
U2_ggaaggaa(T15, T9, T10, X16, X17, gopherA_out_ggaa(T9, T10, X16, X17)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17)
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, T16, T17) → U3_ggaaggaa(T15, T9, T10, T16, T17, gopherA_in_ggaa(T9, T10, T16, T17))
U3_ggaaggaa(T15, T9, T10, T16, T17, gopherA_out_ggaa(T9, T10, T16, T17)) → U4_ggaaggaa(T15, T9, T10, T16, T17, samefringeC_in_gg(T15, T17))
U4_ggaaggaa(T15, T9, T10, T16, T17, samefringeC_out_gg(T15, T17)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, T16, T17)
pB_in_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U5_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
U5_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_out_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)) → pB_out_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17)
U6_gg(T7, T8, T9, T10, pB_out_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17)) → samefringeC_out_gg(cons(T7, T8), cons(T9, T10))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
samefringeC_in_gg(nil, nil) → samefringeC_out_gg(nil, nil)
samefringeC_in_gg(cons(T7, T8), cons(T9, T10)) → U6_gg(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17) → U2_ggaaggaa(T15, T9, T10, X16, X17, gopherA_in_ggaa(T9, T10, X16, X17))
gopherA_in_ggaa(nil, T22, nil, T22) → gopherA_out_ggaa(nil, T22, nil, T22)
gopherA_in_ggaa(cons(T29, T30), T31, X44, X45) → U1_ggaa(T29, T30, T31, X44, X45, gopherA_in_ggaa(T29, cons(T30, T31), X44, X45))
U1_ggaa(T29, T30, T31, X44, X45, gopherA_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherA_out_ggaa(cons(T29, T30), T31, X44, X45)
U2_ggaaggaa(T15, T9, T10, X16, X17, gopherA_out_ggaa(T9, T10, X16, X17)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17)
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, T16, T17) → U3_ggaaggaa(T15, T9, T10, T16, T17, gopherA_in_ggaa(T9, T10, T16, T17))
U3_ggaaggaa(T15, T9, T10, T16, T17, gopherA_out_ggaa(T9, T10, T16, T17)) → U4_ggaaggaa(T15, T9, T10, T16, T17, samefringeC_in_gg(T15, T17))
U4_ggaaggaa(T15, T9, T10, T16, T17, samefringeC_out_gg(T15, T17)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, T16, T17)
pB_in_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U5_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
U5_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_out_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)) → pB_out_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17)
U6_gg(T7, T8, T9, T10, pB_out_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17)) → samefringeC_out_gg(cons(T7, T8), cons(T9, T10))
SAMEFRINGEC_IN_GG(cons(T7, T8), cons(T9, T10)) → U6_GG(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
SAMEFRINGEC_IN_GG(cons(T7, T8), cons(T9, T10)) → PB_IN_GGAAGGAA(T7, T8, X14, X15, T9, T10, X16, X17)
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, X16, X17) → U2_GGAAGGAA(T15, T9, T10, X16, X17, gopherA_in_ggaa(T9, T10, X16, X17))
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, X16, X17) → GOPHERA_IN_GGAA(T9, T10, X16, X17)
GOPHERA_IN_GGAA(cons(T29, T30), T31, X44, X45) → U1_GGAA(T29, T30, T31, X44, X45, gopherA_in_ggaa(T29, cons(T30, T31), X44, X45))
GOPHERA_IN_GGAA(cons(T29, T30), T31, X44, X45) → GOPHERA_IN_GGAA(T29, cons(T30, T31), X44, X45)
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, T16, T17) → U3_GGAAGGAA(T15, T9, T10, T16, T17, gopherA_in_ggaa(T9, T10, T16, T17))
U3_GGAAGGAA(T15, T9, T10, T16, T17, gopherA_out_ggaa(T9, T10, T16, T17)) → U4_GGAAGGAA(T15, T9, T10, T16, T17, samefringeC_in_gg(T15, T17))
U3_GGAAGGAA(T15, T9, T10, T16, T17, gopherA_out_ggaa(T9, T10, T16, T17)) → SAMEFRINGEC_IN_GG(T15, T17)
PB_IN_GGAAGGAA(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U5_GGAAGGAA(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
PB_IN_GGAAGGAA(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → PB_IN_GGAAGGAA(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)
samefringeC_in_gg(nil, nil) → samefringeC_out_gg(nil, nil)
samefringeC_in_gg(cons(T7, T8), cons(T9, T10)) → U6_gg(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17) → U2_ggaaggaa(T15, T9, T10, X16, X17, gopherA_in_ggaa(T9, T10, X16, X17))
gopherA_in_ggaa(nil, T22, nil, T22) → gopherA_out_ggaa(nil, T22, nil, T22)
gopherA_in_ggaa(cons(T29, T30), T31, X44, X45) → U1_ggaa(T29, T30, T31, X44, X45, gopherA_in_ggaa(T29, cons(T30, T31), X44, X45))
U1_ggaa(T29, T30, T31, X44, X45, gopherA_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherA_out_ggaa(cons(T29, T30), T31, X44, X45)
U2_ggaaggaa(T15, T9, T10, X16, X17, gopherA_out_ggaa(T9, T10, X16, X17)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17)
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, T16, T17) → U3_ggaaggaa(T15, T9, T10, T16, T17, gopherA_in_ggaa(T9, T10, T16, T17))
U3_ggaaggaa(T15, T9, T10, T16, T17, gopherA_out_ggaa(T9, T10, T16, T17)) → U4_ggaaggaa(T15, T9, T10, T16, T17, samefringeC_in_gg(T15, T17))
U4_ggaaggaa(T15, T9, T10, T16, T17, samefringeC_out_gg(T15, T17)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, T16, T17)
pB_in_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U5_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
U5_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_out_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)) → pB_out_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17)
U6_gg(T7, T8, T9, T10, pB_out_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17)) → samefringeC_out_gg(cons(T7, T8), cons(T9, T10))
SAMEFRINGEC_IN_GG(cons(T7, T8), cons(T9, T10)) → U6_GG(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
SAMEFRINGEC_IN_GG(cons(T7, T8), cons(T9, T10)) → PB_IN_GGAAGGAA(T7, T8, X14, X15, T9, T10, X16, X17)
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, X16, X17) → U2_GGAAGGAA(T15, T9, T10, X16, X17, gopherA_in_ggaa(T9, T10, X16, X17))
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, X16, X17) → GOPHERA_IN_GGAA(T9, T10, X16, X17)
GOPHERA_IN_GGAA(cons(T29, T30), T31, X44, X45) → U1_GGAA(T29, T30, T31, X44, X45, gopherA_in_ggaa(T29, cons(T30, T31), X44, X45))
GOPHERA_IN_GGAA(cons(T29, T30), T31, X44, X45) → GOPHERA_IN_GGAA(T29, cons(T30, T31), X44, X45)
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, T16, T17) → U3_GGAAGGAA(T15, T9, T10, T16, T17, gopherA_in_ggaa(T9, T10, T16, T17))
U3_GGAAGGAA(T15, T9, T10, T16, T17, gopherA_out_ggaa(T9, T10, T16, T17)) → U4_GGAAGGAA(T15, T9, T10, T16, T17, samefringeC_in_gg(T15, T17))
U3_GGAAGGAA(T15, T9, T10, T16, T17, gopherA_out_ggaa(T9, T10, T16, T17)) → SAMEFRINGEC_IN_GG(T15, T17)
PB_IN_GGAAGGAA(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U5_GGAAGGAA(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
PB_IN_GGAAGGAA(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → PB_IN_GGAAGGAA(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)
samefringeC_in_gg(nil, nil) → samefringeC_out_gg(nil, nil)
samefringeC_in_gg(cons(T7, T8), cons(T9, T10)) → U6_gg(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17) → U2_ggaaggaa(T15, T9, T10, X16, X17, gopherA_in_ggaa(T9, T10, X16, X17))
gopherA_in_ggaa(nil, T22, nil, T22) → gopherA_out_ggaa(nil, T22, nil, T22)
gopherA_in_ggaa(cons(T29, T30), T31, X44, X45) → U1_ggaa(T29, T30, T31, X44, X45, gopherA_in_ggaa(T29, cons(T30, T31), X44, X45))
U1_ggaa(T29, T30, T31, X44, X45, gopherA_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherA_out_ggaa(cons(T29, T30), T31, X44, X45)
U2_ggaaggaa(T15, T9, T10, X16, X17, gopherA_out_ggaa(T9, T10, X16, X17)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17)
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, T16, T17) → U3_ggaaggaa(T15, T9, T10, T16, T17, gopherA_in_ggaa(T9, T10, T16, T17))
U3_ggaaggaa(T15, T9, T10, T16, T17, gopherA_out_ggaa(T9, T10, T16, T17)) → U4_ggaaggaa(T15, T9, T10, T16, T17, samefringeC_in_gg(T15, T17))
U4_ggaaggaa(T15, T9, T10, T16, T17, samefringeC_out_gg(T15, T17)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, T16, T17)
pB_in_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U5_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
U5_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_out_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)) → pB_out_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17)
U6_gg(T7, T8, T9, T10, pB_out_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17)) → samefringeC_out_gg(cons(T7, T8), cons(T9, T10))
GOPHERA_IN_GGAA(cons(T29, T30), T31, X44, X45) → GOPHERA_IN_GGAA(T29, cons(T30, T31), X44, X45)
samefringeC_in_gg(nil, nil) → samefringeC_out_gg(nil, nil)
samefringeC_in_gg(cons(T7, T8), cons(T9, T10)) → U6_gg(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17) → U2_ggaaggaa(T15, T9, T10, X16, X17, gopherA_in_ggaa(T9, T10, X16, X17))
gopherA_in_ggaa(nil, T22, nil, T22) → gopherA_out_ggaa(nil, T22, nil, T22)
gopherA_in_ggaa(cons(T29, T30), T31, X44, X45) → U1_ggaa(T29, T30, T31, X44, X45, gopherA_in_ggaa(T29, cons(T30, T31), X44, X45))
U1_ggaa(T29, T30, T31, X44, X45, gopherA_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherA_out_ggaa(cons(T29, T30), T31, X44, X45)
U2_ggaaggaa(T15, T9, T10, X16, X17, gopherA_out_ggaa(T9, T10, X16, X17)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17)
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, T16, T17) → U3_ggaaggaa(T15, T9, T10, T16, T17, gopherA_in_ggaa(T9, T10, T16, T17))
U3_ggaaggaa(T15, T9, T10, T16, T17, gopherA_out_ggaa(T9, T10, T16, T17)) → U4_ggaaggaa(T15, T9, T10, T16, T17, samefringeC_in_gg(T15, T17))
U4_ggaaggaa(T15, T9, T10, T16, T17, samefringeC_out_gg(T15, T17)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, T16, T17)
pB_in_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U5_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
U5_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_out_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)) → pB_out_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17)
U6_gg(T7, T8, T9, T10, pB_out_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17)) → samefringeC_out_gg(cons(T7, T8), cons(T9, T10))
GOPHERA_IN_GGAA(cons(T29, T30), T31, X44, X45) → GOPHERA_IN_GGAA(T29, cons(T30, T31), X44, X45)
GOPHERA_IN_GGAA(cons(T29, T30), T31) → GOPHERA_IN_GGAA(T29, cons(T30, T31))
From the DPs we obtained the following set of size-change graphs:
SAMEFRINGEC_IN_GG(cons(T7, T8), cons(T9, T10)) → PB_IN_GGAAGGAA(T7, T8, X14, X15, T9, T10, X16, X17)
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, T16, T17) → U3_GGAAGGAA(T15, T9, T10, T16, T17, gopherA_in_ggaa(T9, T10, T16, T17))
U3_GGAAGGAA(T15, T9, T10, T16, T17, gopherA_out_ggaa(T9, T10, T16, T17)) → SAMEFRINGEC_IN_GG(T15, T17)
PB_IN_GGAAGGAA(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → PB_IN_GGAAGGAA(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)
samefringeC_in_gg(nil, nil) → samefringeC_out_gg(nil, nil)
samefringeC_in_gg(cons(T7, T8), cons(T9, T10)) → U6_gg(T7, T8, T9, T10, pB_in_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17))
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17) → U2_ggaaggaa(T15, T9, T10, X16, X17, gopherA_in_ggaa(T9, T10, X16, X17))
gopherA_in_ggaa(nil, T22, nil, T22) → gopherA_out_ggaa(nil, T22, nil, T22)
gopherA_in_ggaa(cons(T29, T30), T31, X44, X45) → U1_ggaa(T29, T30, T31, X44, X45, gopherA_in_ggaa(T29, cons(T30, T31), X44, X45))
U1_ggaa(T29, T30, T31, X44, X45, gopherA_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherA_out_ggaa(cons(T29, T30), T31, X44, X45)
U2_ggaaggaa(T15, T9, T10, X16, X17, gopherA_out_ggaa(T9, T10, X16, X17)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, X16, X17)
pB_in_ggaaggaa(nil, T15, nil, T15, T9, T10, T16, T17) → U3_ggaaggaa(T15, T9, T10, T16, T17, gopherA_in_ggaa(T9, T10, T16, T17))
U3_ggaaggaa(T15, T9, T10, T16, T17, gopherA_out_ggaa(T9, T10, T16, T17)) → U4_ggaaggaa(T15, T9, T10, T16, T17, samefringeC_in_gg(T15, T17))
U4_ggaaggaa(T15, T9, T10, T16, T17, samefringeC_out_gg(T15, T17)) → pB_out_ggaaggaa(nil, T15, nil, T15, T9, T10, T16, T17)
pB_in_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → U5_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_in_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17))
U5_ggaaggaa(T38, T39, T40, X62, X63, T9, T10, X16, X17, pB_out_ggaaggaa(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)) → pB_out_ggaaggaa(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17)
U6_gg(T7, T8, T9, T10, pB_out_ggaaggaa(T7, T8, X14, X15, T9, T10, X16, X17)) → samefringeC_out_gg(cons(T7, T8), cons(T9, T10))
SAMEFRINGEC_IN_GG(cons(T7, T8), cons(T9, T10)) → PB_IN_GGAAGGAA(T7, T8, X14, X15, T9, T10, X16, X17)
PB_IN_GGAAGGAA(nil, T15, nil, T15, T9, T10, T16, T17) → U3_GGAAGGAA(T15, T9, T10, T16, T17, gopherA_in_ggaa(T9, T10, T16, T17))
U3_GGAAGGAA(T15, T9, T10, T16, T17, gopherA_out_ggaa(T9, T10, T16, T17)) → SAMEFRINGEC_IN_GG(T15, T17)
PB_IN_GGAAGGAA(cons(T38, T39), T40, X62, X63, T9, T10, X16, X17) → PB_IN_GGAAGGAA(T38, cons(T39, T40), X62, X63, T9, T10, X16, X17)
gopherA_in_ggaa(nil, T22, nil, T22) → gopherA_out_ggaa(nil, T22, nil, T22)
gopherA_in_ggaa(cons(T29, T30), T31, X44, X45) → U1_ggaa(T29, T30, T31, X44, X45, gopherA_in_ggaa(T29, cons(T30, T31), X44, X45))
U1_ggaa(T29, T30, T31, X44, X45, gopherA_out_ggaa(T29, cons(T30, T31), X44, X45)) → gopherA_out_ggaa(cons(T29, T30), T31, X44, X45)
SAMEFRINGEC_IN_GG(cons(T7, T8), cons(T9, T10)) → PB_IN_GGAAGGAA(T7, T8, T9, T10)
PB_IN_GGAAGGAA(nil, T15, T9, T10) → U3_GGAAGGAA(T15, gopherA_in_ggaa(T9, T10))
U3_GGAAGGAA(T15, gopherA_out_ggaa(T16, T17)) → SAMEFRINGEC_IN_GG(T15, T17)
PB_IN_GGAAGGAA(cons(T38, T39), T40, T9, T10) → PB_IN_GGAAGGAA(T38, cons(T39, T40), T9, T10)
gopherA_in_ggaa(nil, T22) → gopherA_out_ggaa(nil, T22)
gopherA_in_ggaa(cons(T29, T30), T31) → U1_ggaa(gopherA_in_ggaa(T29, cons(T30, T31)))
U1_ggaa(gopherA_out_ggaa(X44, X45)) → gopherA_out_ggaa(X44, X45)
gopherA_in_ggaa(x0, x1)
U1_ggaa(x0)
PB_IN_GGAAGGAA(nil, T15, T9, T10) → U3_GGAAGGAA(T15, gopherA_in_ggaa(T9, T10))
POL(PB_IN_GGAAGGAA(x1, x2, x3, x4)) = 2·x1 + 2·x2 + 2·x3 + 2·x4
POL(SAMEFRINGEC_IN_GG(x1, x2)) = 2·x1 + 2·x2
POL(U1_ggaa(x1)) = x1
POL(U3_GGAAGGAA(x1, x2)) = 2·x1 + 2·x2
POL(cons(x1, x2)) = x1 + x2
POL(gopherA_in_ggaa(x1, x2)) = x1 + x2
POL(gopherA_out_ggaa(x1, x2)) = x1 + x2
POL(nil) = 2
SAMEFRINGEC_IN_GG(cons(T7, T8), cons(T9, T10)) → PB_IN_GGAAGGAA(T7, T8, T9, T10)
U3_GGAAGGAA(T15, gopherA_out_ggaa(T16, T17)) → SAMEFRINGEC_IN_GG(T15, T17)
PB_IN_GGAAGGAA(cons(T38, T39), T40, T9, T10) → PB_IN_GGAAGGAA(T38, cons(T39, T40), T9, T10)
gopherA_in_ggaa(nil, T22) → gopherA_out_ggaa(nil, T22)
gopherA_in_ggaa(cons(T29, T30), T31) → U1_ggaa(gopherA_in_ggaa(T29, cons(T30, T31)))
U1_ggaa(gopherA_out_ggaa(X44, X45)) → gopherA_out_ggaa(X44, X45)
gopherA_in_ggaa(x0, x1)
U1_ggaa(x0)
PB_IN_GGAAGGAA(cons(T38, T39), T40, T9, T10) → PB_IN_GGAAGGAA(T38, cons(T39, T40), T9, T10)
gopherA_in_ggaa(nil, T22) → gopherA_out_ggaa(nil, T22)
gopherA_in_ggaa(cons(T29, T30), T31) → U1_ggaa(gopherA_in_ggaa(T29, cons(T30, T31)))
U1_ggaa(gopherA_out_ggaa(X44, X45)) → gopherA_out_ggaa(X44, X45)
gopherA_in_ggaa(x0, x1)
U1_ggaa(x0)
PB_IN_GGAAGGAA(cons(T38, T39), T40, T9, T10) → PB_IN_GGAAGGAA(T38, cons(T39, T40), T9, T10)
gopherA_in_ggaa(x0, x1)
U1_ggaa(x0)
gopherA_in_ggaa(x0, x1)
U1_ggaa(x0)
PB_IN_GGAAGGAA(cons(T38, T39), T40, T9, T10) → PB_IN_GGAAGGAA(T38, cons(T39, T40), T9, T10)
From the DPs we obtained the following set of size-change graphs: